AtomFreeDecls(X)
== (i, x:Id. AtomFree(Type;((X.2.2.2.2.2).1)(i,x)))
== & (i:Id, k:Knd. AtomFree(Type;((X.2.2.2.2.2.2.2.2.2).1)(k,i))) 

latex

---

clarification:

EVal-atom-free{i:l}
EVal-atom-free(X)
== (i:Id, x:Id. atom-free{1:n}(Type{i}; (((X.2.2.2.2.2).1)(i,x))))
== & (i:Id, k:Knd. atom-free{1:n}(Type{i}; (((X.2.2.2.2.2.2.2.2.2).1)(k,i)))) 

latex

Definitions	t.2, t.1, f(a), Type, Knd, x:A. B(x), Id, P & Q
FDL editor aliases	EVal-atom-free